package interfaces.gestores;

import interfaces.ITecnico;
import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;

@Init ({""})
@Inv ({""})


public interface IGestorTecnicosWithModel extends IGestorTecnicosModel,
		IGestorTecnicos {
	
	@Pre ({"t!=null #NullPointerException","estaTecnico(t)"})
	@Pos ({"!estaTecnico(t)"})
	public void bajaTecnico(ITecnico t);
	
	@Pre ({"tecnico!=null && nuevoTecnico != null #NullPointerException", "tecnico.getID() == nuevoTecnico.getID() && estaTecnico(tecnico)"})
	@Pos ({"estaTecnico(nuevoTecnico) && !estaTecnico(tecnico)"})
	public void modificarTecnico(ITecnico tecnico, ITecnico nuevoTecnico);
	
	@Pre ({"nuevoTecnico!=null #NullPointerException", "!estaTecnico(nuevoTecnico)"})
	@Pos ({"estaTecnico(nuevoTecnico)"})
	public void altaTecnico(ITecnico nuevoTecnico);
}

